$\forall$$a$:Atom1, $A$:Type, $v$:$A$+Unit. AtomFree(Type;$A$) $\Rightarrow$ isl($v$) $\Rightarrow$ outl($v$):$A$$>>$$a$ $\Rightarrow$ $v$:$A$+Unit$>>$$a$